(***************************************************************************
 * Cast-Free Featherweight Java
 *
 * Bruno De Fraine, with help from Erik Ernst and Mario Sudholt, Summer 2008
 ***************************************************************************)

Require Import AdditionalTactics.
Require Import Metatheory.
Require Import FJ_Definitions.
Require Import FJ_Facts.
Require Import FJ_Properties.

(* The classic Pair example from the FJ paper *)

Variable a : scname.
Variable b : scname.
Variable pair : scname.

Definition obj := t_C Object.
Definition A := t_C a.
Definition B := t_C b.
Definition Pair := t_C pair.

Hypothesis A_fresh: obj <> A.
Hypothesis B_fresh: obj <> B /\ A <> B.

Hypothesis Pair_fresh : 
  obj <> Pair /\ A <> Pair /\ B <> Pair.

Lemma A_fresh_not: 
  ~(obj = A).
Proof.
  exact A_fresh.
Qed.

Lemma B_fresh_not: 
  ~(obj = B \/ A = B).
Proof.
  destruct B_fresh.
  tauto.
Qed.

Lemma Pair_fresh_not: 
  ~(obj = Pair \/ A = Pair \/ B = Pair).
Proof.
  destruct Pair_fresh.
  destruct H0.
  tauto.
Qed.

Hint Local Resolve A_fresh_not B_fresh_not Pair_fresh_not.

Variable fst : fieldname.
Variable snd : fieldname.
Hypothesis fst_neq_snd : fst <> snd.
Variable setfst : mname.
Variable newfst : var.
Hypothesis newfst_neq_this : this <> newfst.

Definition pair_flds' : fdecls := 
  (obj,fst) :: (obj,snd) :: nil.
Definition pair_flds : fenv := 
  (fst,obj) :: (snd,obj) :: nil.

Definition setfst_env : tenv := 
  (newfst,obj) :: nil.

Definition new_pair (x:exp) (y:exp) := 
  e_new Pair (x :: y :: nil).

Definition setfst_body : exp := 
  new_pair (e_var newfst) (e_field (e_var this) snd).

Definition pair_mths' : mdecls := 
  (nil,Pair,setfst,setfst_env,setfst_body) :: nil.
Definition pair_mths : menv := 
  (setfst,(nil,Pair,setfst_env,setfst_body)) :: nil.

Definition class_decls : cdecls := 
  (a,Object,nil,(a,nil),nil,nil) 
    :: (b,Object,nil,(b,nil),nil,nil) 
    :: (pair,Object,pair_flds',(pair,pair_flds'),pair_mths',nil) 
    :: nil.

Hypothesis ct_fix: CT = make_cenv class_decls.

(* The class table will now have been translated from

(a,Object,nil,(a,nil),nil,nil) :: 
(b,Object,nil,(b,nil),nil,nil) :: 
(pair,Object,pair_flds',(pair,pair_flds'),pair_mths',nil) :: nil.

   into

(a,(Object,nil,(a,nil),nil,nil)) ::
(b,(Object,nil,(b,nil),nil,nil)) ::
(pair,(Object,pair_flds,(pair,pair_flds),pair_mths,nil)) :: nil. 

   Inspect CT by evaluating

Compute make_cenv class_decls.
*)

Module ExNoObj: NoObj.

Lemma ct_noobj: 
  no_binds Object CT.
Proof.
  rewrite ct_fix.
  assert (H0 : no_binds Object (nil:cenv)).
  unfold no_binds.
  auto.
  unfold class_decls.
  apply nobinds_cons with (y:=pair) 
        (b:=(Object,pair_flds,(pair,pair_flds),pair_mths,nil)) in H0.
  apply nobinds_cons with (y:=b) 
        (b:=(Object,nil,(b,nil),nil,nil)) in H0.
  apply nobinds_cons with (y:=a) 
        (b:=(Object,nil,(a,nil),nil,nil)) in H0.
  assumption.
      assert (HA := A_fresh_not).
      unfold not in *.
      intro.
      apply HA.
      unfold obj.
      unfold A.
      rewrite H.
      reflexivity.
    assert (HB := B_fresh_not).
    unfold not in *.
    intro.
    apply HB.
    left.
    unfold obj.
    unfold B.
    rewrite H.
    reflexivity.
  assert (HP := Pair_fresh_not).
  unfold not in *.
  intro.
  apply HP.
  left.
  unfold obj.
  unfold Pair.
  rewrite H.
  reflexivity.
Qed.

End ExNoObj.

Lemma ct_a: 
  binds a (Object,nil,(a,nil),nil,nil) CT.
Proof.
  rewrite ct_fix in |- *. 
  apply binds_first.
Qed.

Lemma ct_b: 
  binds b (Object,nil,(b,nil),nil,nil) CT.
Proof.
  rewrite ct_fix in |- *. 
  apply binds_other.
  apply binds_first.
  assert (HB := B_fresh_not).
  unfold not in *.
  intro.
  apply HB.
  right.
  unfold A.
  unfold B.
  rewrite H.
  reflexivity.
Qed.

Lemma ct_pair: 
  binds pair (Object,pair_flds,(pair,pair_flds),pair_mths,nil) CT.
Proof.
  rewrite ct_fix in |- *.
  apply binds_other.
    apply binds_other.
      apply binds_first.
    assert (HP := Pair_fresh_not).
    unfold not in *.
    intro.
    apply HP.
    right. right.
    unfold B.
    unfold Pair.
    rewrite H.
    reflexivity.
  assert (HP := Pair_fresh_not).
  unfold not in *.
  intro.
  apply HP.
  right. left.
  unfold A.
  unfold Pair.
  rewrite H.
  reflexivity.
Qed.

Hint Local Resolve ct_a ct_b ct_pair fst_neq_snd newfst_neq_this.

Hint Unfold no_binds.

Lemma ex_ok_setfst_env : 
  ok ((this,Pair)::setfst_env).
Proof.
  pose newfst_neq_this.
  unfold setfst_env in |- *.  
  auto using nobinds_nil, nobinds_cons.
Qed.

Lemma pair_pair_flds : 
  fields Pair pair_flds.
Proof.
  assert (H := ct_pair).
  unfold Pair.
  change pair_flds with (nil ++ pair_flds) in |- *;
  eauto.
Qed.

Hint Local Resolve ex_ok_setfst_env pair_pair_flds.

Module Import Facts1 := NoObjFacts ExNoObj.

Lemma imgs_list_app:
  forall (T:Type) (x:atom) (y:T) l,
    imgs ((x,y) :: l) = y :: (imgs l).
Proof.
  intros.
  eauto.
Qed.

Lemma imgs_nil:
  imgs (nil:tenv) = nil.
Proof.
  unfold imgs.
  unfold List.map.
  reflexivity.
Qed.

Lemma ex_ok_setfst: 
  ok_meth nil Pair setfst setfst_env setfst_body Pair.
Proof.
  assert (typeis_qcname Pair).
    unfold Pair; eauto.
  unfold ok_meth.
  exists Pair.
  split. unfold Pair; auto.
  split. unfold setfst_body.
    unfold Pair.
    eapply wt_sub; eauto.
    apply (t_new _ pair_flds _ _ _ _ (imgs pair_flds)); eauto.
      unfold pair_flds.
      apply ca_cons.
        unfold obj. 
        eauto.
      apply ca_cons.
        unfold obj.
        eauto.
      apply ca_nil.
  eapply wts_cons; eauto.
    eapply wts_cons; eauto.
    apply wt_sub with (t:=obj); eauto.
    apply (t_field _ Pair Pair _ _ obj Pair _ _ _); eauto.
      unfold field. 
      exists pair_flds; eauto.
      unfold pair_flds.
      apply binds_other; eauto.
      apply binds_first.
      unfold obj; unfold Pair; eauto.
      unfold Pair; eauto.
      apply t_var; eauto.
      apply binds_first.
    apply wt_sub with (t:=obj); eauto.
    eapply t_var; eauto.
    unfold setfst_env.
    apply binds_other; eauto.
    apply binds_first.
    split. unfold Pair. eauto.
    split. unfold setfst_env. unfold Pair.
      rewrite imgs_list_app.
      assert (Hi : imgs (nil:tenv) = nil).
        unfold imgs.
        unfold List.map.
        reflexivity.
      rewrite Hi.
      unfold ok_types.
      split; eauto.
    split. 
      assert (Hi : imgs (nil:benv) = nil).
        unfold imgs.
        unfold List.map.
        reflexivity.
      rewrite Hi.
      unfold scnames2types.
      unfold List.map.
      eauto.
    split.
      reflexivity.
    intros.
    split.
      assert (Hct := ExNoObj.ct_noobj).
      inversion H0; subst; eauto.
      assert (H4 := ct_pair).
      apply binds_fun with (1:=H4)in H3.
      subst injections.
      inversion H1; subst.
      exfalso.
      apply binds_nobinds with (1:=H3) (2:=Hct); eauto.
      exfalso.
      apply binds_nobinds with (1:=H3) (2:=Hct); eauto.
    split.
      assert (Hct := ExNoObj.ct_noobj).
      inversion H0; subst; eauto.
      assert (H4 := ct_pair).
      apply binds_fun with (1:=H4)in H3.
      subst injections.
      inversion H1; subst.
      exfalso.
      apply binds_nobinds with (1:=H3) (2:=Hct); eauto.
      exfalso.
      apply binds_nobinds with (1:=H3) (2:=Hct); eauto.
    assert (Hct := ExNoObj.ct_noobj).
    inversion H0; subst; eauto.
    assert (H4 := ct_pair).
    apply binds_fun with (1:=H4)in H3.
    subst injections.
    inversion H1; subst.
    exfalso.
    apply binds_nobinds with (1:=H3) (2:=Hct); eauto.
    exfalso.
    apply binds_nobinds with (1:=H3) (2:=Hct); eauto.
Qed.

Lemma ex_ok_pair: 
  ok_tclass pair Object pair_flds (pair,pair_flds) pair_mths nil.
Proof.
  unfold ok_tclass.
  exists A, nil.
  simpl.
  split; eauto.
  split; eauto.
  split. unfold pair_mths.
  apply fa_cons.
    apply fa_nil.
  unfold ok_meth'.
  apply ex_ok_setfst.
  split; eauto.
  apply fa_nil.
Qed.

Module ExOkTable.

Lemma ok_ct: ok_cenv CT.
Proof.
  rewrite ct_fix in |- *.
  unfold ok_cenv in |- *.
  split.
  apply ok_cons. apply ok_cons. apply ok_cons. 
  apply ok_nil; eauto. eauto.
  unfold no_binds. unfold get. apply eq_atom_false.
  assert (He := Pair_fresh_not).
  unfold not in He. unfold not. intro. apply He.
  right. right. unfold B. unfold Pair. rewrite H. reflexivity.
  assert (Hb := B_fresh_not).
  unfold not in Hb.
  assert (a <> b). unfold not. intro. apply Hb.
  right. unfold A. unfold B. rewrite H. reflexivity.
  assert (Hp := Pair_fresh_not).
  unfold not in Hp.
  assert (a <> pair). unfold not. intro. apply Hp.
  right. left. unfold A. unfold Pair. rewrite H0. reflexivity.
  unfold cdecl2csin.
  unfold no_binds. unfold get. rewrite eq_atom_false.
  rewrite eq_atom_false. reflexivity.
  assumption.
  assumption.
  apply fa_cons.
  apply fa_cons.
  apply fa_cons.
  apply fa_nil.
  unfold ok_tclass' in |- *; apply ex_ok_pair.
  unfold ok_tclass' in |- *; apply ok_class_empty.
  unfold ok_tclass' in |- *; apply ok_class_empty.
Qed.

End ExOkTable.

Module ExHyps: Hyps.

Definition ct_noobj := ExNoObj.ct_noobj.
Definition ok_ct := ExOkTable.ok_ct.

End ExHyps.

Module Import Props1 := Properties ExHyps.

(* new Pair(a, b).snd -> b *)
Lemma ex_step_field: 
  forall a b, 
    eval (e_field (new_pair a b) snd) b.
Proof.
  intros.
  unfold new_pair in |- *.
  eapply eval_field.
  apply pair_pair_flds.
  unfold pair_flds in |- *; simpl.
  apply z_cons.
  apply z_cons.
  apply z_nil.
  eauto using binds_first, binds_other.
Qed.

(* context is (t_C Object) *)
Lemma ex_type_field:
  typing nil nil (e_field (new_pair (e_new A nil) (e_new B nil)) snd) 
         obj Pair.
Proof.
  apply (t_field _ Pair Pair _ _ obj Pair _ _ _).
    unfold Pair; auto.
  unfold field. 
  exists pair_flds; auto.
  unfold pair_flds. 
  apply binds_other; auto.
  apply binds_first. 
  unfold Pair; auto.
  unfold obj; auto.
  unfold Pair; auto.
  unfold Pair; unfold new_pair.
    apply (t_new _ pair_flds _ _ _ _ (imgs pair_flds)); auto.
  unfold pair_flds.
  apply ca_cons.
    unfold obj; auto.
  apply ca_cons.
    unfold obj; auto.
  apply ca_nil.
  apply wts_cons; auto.  
  apply wts_cons; auto.
  apply wt_sub with (t:=B); auto.
  apply (t_new _ nil _ _ _ _ (imgs nil)); auto.
  assert (Hct := ct_fix).
  unfold B. 
  assert (binds b (Object, nil, (b, nil), nil, nil) CT); auto.
  assert (Hf := f_tobject).
  assert (fields (t_C b) (nil ++ nil)).
  apply (f_tclass _ _ _ _ _ _ _ H Hf); auto.
  simpl in H0.
  assumption.
  unfold B; unfold obj.
  assert (Hct := ct_fix).
  assert (binds b (Object, nil, (b, nil), nil, nil) CT); auto.
  apply (wt_sub _ _ _ A _ _); auto.
  apply (t_new _ nil _ _ _ _ (imgs nil)); auto.
  unfold A.
  assert (binds a (Object, nil, (a, nil), nil, nil) CT).
    auto.
  assert (Hf := f_tobject).
  assert (fields (t_C a) (nil ++ nil)).
  apply (f_tclass _ _ _ _ _ _ _ H0 Hf); auto.
  assumption.
Qed.

Lemma ex_subst_body: 
  forall a b c,
    subst_exp ((this,new_pair a b)::(newfst,c)::nil) setfst_body =
    new_pair c (e_field (new_pair a b) snd).
Proof.
  intros.
  simpl in |- *.
  rewrite eq_atom_true in |- *.
  rewrite eq_atom_true in |- *.
  rewrite eq_atom_false in |- *.
  reflexivity.
  auto.
Qed.

(* new Pair(a, b).setfst(c) -> new Pair(c, b) *)
Lemma ex_step_meth: 
  forall a b c,
    eval (e_meth (new_pair a b) setfst nil (c::nil)) 
         (new_pair c (e_field (new_pair a b) snd)).
Proof.
  intros.
  rewrite <- ex_subst_body in |- *.
  unfold new_pair in |- *.
  eapply eval_meth.
  unfold Pair.
  eapply mt_tclass; eauto.
  unfold pair_mths.
  apply binds_first.
  unfold setfst_env in |- *; simpl.
  apply z_cons.
  apply z_nil.
  apply z_nil.
  eauto.
Qed.
